Inference at * 1 2 1 
Iof proof for Lemma decidable equal int seg:



1. i : 
2. j : 
3. x : {i..j}
4. y : {i..j}
5. (x = y)
  (x = y) 

latex

 by (Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok SupInf:t) inil_term)
 b

latex

 .

Definitions

t  T, {i..j}